//This file was generated from (Academic) UPPAAL 4.1.18 (rev. 5444), November 2013

/*
true
*/
E<> router.ticketRouterOpen

/*
true
*/
E<> (router.Ticket1000 || router.Ticket30 || router.TicketFull )

/*
false: the line can always be damaged
*/
router.ticketRouterOpen --> ! router.ticketRouterOpen

/*
false: the line can always be damaged
*/
(router.Ticket30 or router.Ticket1000 or router.TicketFull) --> router.TicketClose

/*
false: the line can always be damaged
*/
router.Ticket30 --> router.TicketClose

/*
false: the line can always be damaged
*/
router.TicketFull --> router.TicketClose

/*
false: the line can always be damaged
*/
router.Ticket1000 --> router.TicketClose

/*
true: you can close a ticket in less than 180 sec
*/
E<> router.nticket > 0 && router.cRouterTicketOpen < 180 && ! router.ticketRouterOpen

/*
true: you can close a ticket in more than 120 sec
*/
E<> router.nticket > 0 && router.cTicketOpen >= 120 && ! router.ticketOpen

/*
false: you cannot close a ticket in less than 120
*/
E<> router.nticket > 0 && router.cRouterTicketOpen < 120 && ! router.ticketRouterOpen

/*
true : you cannot close a ticket before 2 minutes
*/
router.ticketOpen --> (router.cTicketOpen < 120 imply router.ticketOpen)

/*
true
*/
A[] ! deadlock

/*
true
*/
E<> ! deadlock
